SAMELE.LSP[F81,JMC] - www.SailDart.org

perm filename SAMELE.LSP[F81,JMC] blob sn#622592 filedate 1981-11-07 generic text, type C, neo UTF8

COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 samele.lsp[f81,jmc]	ekl axioms for the same length predicate
C00003 00003
C00007 ENDMK
C⊗;
;;; samele.lsp[f81,jmc]	ekl axioms for the same length predicate

(get-proofs lispax)
(proof samelength)
(context lispax#1:*)

(decl (sl) |ground⊗ground→truthval| constant)

(axiom |∀u v.sl(u,v) ≡ null(u)∧null(v) ∨ ¬null(u)∧¬null(v)∧sl(cdr(u),cdr(v))|)